Nuprl Lemma : append_assoc_sq
11,40
postcript
pdf
as
,
bs
,
cs
:(top List). sqequal(append(append(
as
;
bs
);
cs
); append(
as
; append(
bs
;
cs
)))
latex
Definitions
x
:
A
.
B
(
x
)
,
append(
as
;
bs
)
,
Y
,
t
T
Lemmas
top
wf
origin
as,bs,cs:(top List). sqequal(append(append(as; bs); cs); append(as; append(bs; cs))) as,bs,cs:(top List). sqequal(append(append(as; bs); cs); append(as; append(bs; cs))) x:A. B(x)
T